

We choose to express the toxicology properties in computation tree logic (CTL).
\comment{per quale motivo CTL e non altri?}
We recall here the basic concepts of CTL, we provide the formal definition of the syntax but we only give some intuitions on the semantics, which is formally defined in \cite{Emerson}.

\begin{definition}[CTL]
Let $a \in A$ be an atomic proposition, a CTL formula is defined as: 

$$
\varphi: \bot \mid a \mid \neg \varphi \mid \varphi \vee \varphi \mid \varphi \wedge \varphi \mid \varphi \rightarrow \varphi \mid \esiste \x \varphi \mid \esiste \globally \varphi \mid \varphi \esiste \until \varphi \mid \esiste \finally \varphi \mid \all \globally \varphi \mid \all \finally \varphi
$$
% Let $K= (S,\rightarrow, s_0, A,\nu)$ be a Kripke structure.
% We define the semantic of every CTL formula $\varphi$ over A wrt $K$ as a set of states $\enc{\varphi}_K$:
% 
% 
% $$
% \begin{array}{lcl}
%  \enc{a}_K& = &\nu(a) \text{ for } a \in A \\
%  \enc{\neg \varphi}_K&=& S \setminus \enc{\varphi}_K \\
% \enc{\varphi_1 \vee \varphi_2}_K& =& \enc{\varphi_1}_K \cup \enc{\varphi_2}_K \\ 
% \enc{\esiste \x \varphi}_K&=&\{ s \mid \exists t, s \rightarrow t \text{ and } t \in \enc{\varphi}_K\} \\
% \enc{\esiste \globally \varphi}_K &=& \{ s \mid \text{there exists a run } \rho \text{ s.t. } \rho(0)=s \text{ and } \rho(i)\in \enc{\varphi}_K, \forall i \geq 0\}\\
% \enc{\varphi_1 \esiste \until \varphi_2}_K &=& \{s \mid  \text{there exists a run } \rho \text{ s.t. } \rho(0)=s, \\
% && \exists k\geq 0,
% \rho(i)\in \enc{\varphi_1}_K \forall i < k \text{ and } \rho(k) \in \enc{\varphi_2}_K\}
% \end{array}
% $$
% 
% We say that $K$ satisfies $\varphi$ ( $K \models \varphi$) iff $s_0 \in \enc{\varphi}_K$
\end{definition}


CTL is used to state properties on branching time structures: its formulae can reason about multiple runs at the same time.
The logic uses usual boolean operators, path quantifiers and temporal operators. Boolean operators have the expected semantics. Path quantifiers can be of two kinds $\all$ and $\esiste$. $\all \varphi$ means  that $\varphi$ has to hold on all paths starting from the current state, while $\esiste \varphi$ stands for there exists at least one path starting from the current state where $\varphi$ holds.
We have four temporal operators: $\x, \globally, \finally$ and $\until$. 
$\x \varphi$ holds if $\varphi$ is true at the \emph{next} state. $\globally \varphi$ means  that $\varphi$ has to \emph{globally} hold on the entire subsequent path. $\finally \varphi$ stands for eventually (or \emph{finally}) $\varphi$ has to hold (at some point on the subsequent path).  And finally, $\varphi_1 \until \varphi_2$ means that $\varphi_1$ has to hold at least \emph{until} at some position $\varphi_2$ holds. 





\begin{example}[Glucose metabolism]
Take our example of the introduction.
\begin{enumerate}
 \item Is it true that if  glycemia  is  high there exists a regulation process that lowers glycemia to the equilibrium state?
$$\esiste \finally (Glucose, 2) \rightarrow \all \finally (Glucose, 1) $$
 \item  Is it true that it is not possible to have glucagon and insuline active at the same time?
$$\all \globally \neg ((Glycogenolysis, 1) \wedge (Glycogenesis, 1))$$
 \item Is it true that eating a sweetener wil not cause hunger? 
$$\esiste \finally ((Sugar, 1) \vee (Aspartame, 1)) \rightarrow \all \finally (Hunger,0) $$
\end{enumerate}


 
\end{example}
